(set-logic QF_UFLRA)
(set-info :source |CPAchecker with bounded model checking on SV-COMP14 program using MathSAT5, submitted by Philipp Wendler, http://cpachecker.sosy-lab.org|)
(set-info :smt-lib-version 2.0)
(set-info :category "industrial")


(define-fun _2 () Bool false)
(declare-fun |__ADDRESS_OF_intel_menlow_module_init::__cil_tmp11| () Real)
(declare-fun |intel_menlow_module_init::result@3| () Real)
(declare-fun |__ADDRESS_OF_main::tmp___1| () Real)
(declare-fun |__ADDRESS_OF_intel_menlow_module_init::__cil_tmp7| () Real)
(declare-fun |__ADDRESS_OF_intel_menlow_module_init::__cil_tmp6| () Real)
(declare-fun |intel_menlow_module_init::__cil_tmp7@2| () Real)
(declare-fun |__ADDRESS_OF_main::var_memory_get_max_bandwidth_0_p1| () Real)
(declare-fun __ADDRESS_OF_intel_menlow_attr_lock () Real)
(declare-fun |intel_menlow_module_init::__cil_tmp9@3| () Real)
(declare-fun *unsigned_long_long_int@1 (Real) Real)
(declare-fun |intel_menlow_module_init::result@4| () Real)
(declare-fun |__ADDRESS_OF_main::var_group2| () Real)
(declare-fun __string__ (Real) Real)
(declare-fun |intel_menlow_module_init::__cil_tmp11@2| () Real)
(declare-fun |__ADDRESS_OF___VERIFIER_fake_alloc*(void)[0]#0| () Real)
(declare-fun |__ADDRESS_OF_main::var_memory_get_cur_bandwidth_1_p1| () Real)
(declare-fun __ADDRESS_OF_intel_menlow_register_sensor () Real)
(declare-fun |__ADDRESS_OF_main::tmp| () Real)
(declare-fun |__ADDRESS_OF_intel_menlow_module_init::__cil_tmp10| () Real)
(declare-fun |__ADDRESS_OF_intel_menlow_module_init::__cil_tmp5| () Real)
(declare-fun |main::tmp@3| () Real)
(declare-fun acpi_disabled@2 () Real)
(declare-fun |intel_menlow_module_init::__cil_tmp11@3| () Real)
(declare-fun |__ADDRESS_OF_intel_menlow_module_init::enable| () Real)
(declare-fun |__ADDRESS_OF_main::var_group1| () Real)
(declare-fun |__ADDRESS_OF___VERIFIER_fake_alloc*(void)[0]#2| () Real)
(declare-fun |intel_menlow_module_init::__cil_tmp10@2| () Real)
(declare-fun |intel_menlow_module_init::__cil_tmp6@3| () Real)
(declare-fun |intel_menlow_module_init::__cil_tmp9@2| () Real)
(declare-fun __BASE_ADDRESS_OF__ (Real) Real)
(declare-fun |__ADDRESS_OF___VERIFIER_fake_alloc*(void)[0]#1| () Real)
(declare-fun |intel_menlow_module_init::status@3| () Real)
(declare-fun ___pc@4 () Real)
(declare-fun |__ADDRESS_OF_intel_menlow_module_init::__cil_tmp9| () Real)
(declare-fun acpi_walk_namespace (Real Real Real Real Real Real Real) Real)
(declare-fun ___pc@3 () Real)
(declare-fun __ADDRESS_OF_intel_menlow_memory_driver () Real)
(declare-fun __ADDRESS_OF_intel_menlow_memory_ids () Real)
(declare-fun |intel_menlow_module_init::__cil_tmp8@3| () Real)
(declare-fun |__ADDRESS_OF_intel_menlow_module_init::status| () Real)
(declare-fun |intel_menlow_module_init::status@4| () Real)
(declare-fun __ADDRESS_OF____pc () Real)
(declare-fun __ADDRESS_OF_acpi_disabled () Real)
(declare-fun |__ADDRESS_OF_intel_menlow_module_init::__cil_tmp4| () Real)
(declare-fun __ADDRESS_OF_intel_menlow_attr_list () Real)
(declare-fun |intel_menlow_module_init::__cil_tmp8@2| () Real)
(declare-fun |intel_menlow_module_init::__retval__@2| () Real)
(declare-fun |__ADDRESS_OF_intel_menlow_module_init::result| () Real)
(declare-fun |intel_menlow_module_init::__cil_tmp10@3| () Real)
(declare-fun |intel_menlow_module_init::enable@2| () Real)
(declare-fun acpi_bus_register_driver (Real) Real)
(declare-fun __ADDRESS_OF_memory_cooling_ops () Real)
(declare-fun |__ADDRESS_OF_intel_menlow_module_init::__cil_tmp12| () Real)
(declare-fun |__ADDRESS_OF_intel_menlow_module_init::__cil_tmp8| () Real)
(declare-fun acpi_evaluate_integer (Real Real Real Real) Real)
(declare-fun |intel_menlow_module_init::__cil_tmp12@3| () Real)
(declare-fun |__ADDRESS_OF_main::tmp___0| () Real)
(declare-fun |intel_menlow_module_init::__cil_tmp5@3| () Real)
(declare-fun |intel_menlow_module_init::__cil_tmp12@2| () Real)
(declare-fun |__ADDRESS_OF_main::var_memory_set_cur_bandwidth_2_p1| () Real)
(declare-fun intel_menlow_register_sensor@1 () Real)
(declare-fun |intel_menlow_module_init::__cil_tmp7@3| () Real)
(declare-fun |intel_menlow_module_init::__cil_tmp4@3| () Real)
(declare-fun |*unsigned_int_((void)*,_unsigned_int,_(void)*,_((void)*)*)@1| (Real) Real)
(define-fun _7 () Real 0)
(define-fun _8 () Real __ADDRESS_OF____pc)
(define-fun _9 () Real (__BASE_ADDRESS_OF__ _8))
(define-fun _10 () Bool (= _8 _9))
(define-fun _11 () Real ___pc@3)
(define-fun _12 () Bool (= _11 _7))
(define-fun _13 () Bool (and _10 _12))
(define-fun _14 () Real 1)
(define-fun _16 () Bool (and _12 _13))
(define-fun _19 () Real __ADDRESS_OF_acpi_disabled)
(define-fun _20 () Real (__BASE_ADDRESS_OF__ _19))
(define-fun _21 () Bool (= _19 _20))
(define-fun _22 () Bool (and _16 _21))
(define-fun _23 () Real __ADDRESS_OF_memory_cooling_ops)
(define-fun _24 () Real (__BASE_ADDRESS_OF__ _23))
(define-fun _25 () Bool (= _23 _24))
(define-fun _26 () Bool (<= _23 _7))
(define-fun _27 () Bool (not _26))
(define-fun _28 () Bool (and _25 _27))
(define-fun _29 () Bool (and _22 _28))
(define-fun _30 () Real __ADDRESS_OF_intel_menlow_memory_ids)
(define-fun _31 () Real (__BASE_ADDRESS_OF__ _30))
(define-fun _32 () Bool (= _30 _31))
(define-fun _35 () Real (- 24))
(define-fun _36 () Bool (<= _23 _35))
(define-fun _37 () Bool (not _36))
(define-fun _38 () Real (- 1))
(define-fun _39 () Real (* (- 1) _30))
(define-fun _40 () Real (+ _23 _39))
(define-fun _41 () Bool (<= _40 _35))
(define-fun _42 () Bool (and _37 _41))
(define-fun _43 () Bool (and _32 _42))
(define-fun _44 () Bool (and _29 _43))
(define-fun _45 () Real __ADDRESS_OF_intel_menlow_memory_driver)
(define-fun _46 () Real (__BASE_ADDRESS_OF__ _45))
(define-fun _47 () Bool (= _45 _46))
(define-fun _50 () Real (- 48))
(define-fun _51 () Bool (<= _30 _50))
(define-fun _52 () Bool (not _51))
(define-fun _53 () Real (* (- 1) _45))
(define-fun _54 () Real (+ _30 _53))
(define-fun _55 () Bool (<= _54 _50))
(define-fun _56 () Bool (and _52 _55))
(define-fun _57 () Bool (and _47 _56))
(define-fun _58 () Bool (and _44 _57))
(define-fun _59 () Real __ADDRESS_OF_intel_menlow_attr_list)
(define-fun _60 () Real (__BASE_ADDRESS_OF__ _59))
(define-fun _61 () Bool (= _59 _60))
(define-fun _64 () Real (- 349))
(define-fun _65 () Bool (<= _45 _64))
(define-fun _66 () Bool (not _65))
(define-fun _67 () Real (* (- 1) _59))
(define-fun _68 () Real (+ _45 _67))
(define-fun _69 () Bool (<= _68 _64))
(define-fun _70 () Bool (and _66 _69))
(define-fun _71 () Bool (and _61 _70))
(define-fun _72 () Bool (and _58 _71))
(define-fun _73 () Real __ADDRESS_OF_intel_menlow_attr_lock)
(define-fun _74 () Real (__BASE_ADDRESS_OF__ _73))
(define-fun _75 () Bool (= _73 _74))
(define-fun _78 () Real (- 16))
(define-fun _79 () Bool (<= _59 _78))
(define-fun _80 () Bool (not _79))
(define-fun _81 () Real (* (- 1) _73))
(define-fun _82 () Real (+ _59 _81))
(define-fun _83 () Bool (<= _82 _78))
(define-fun _84 () Bool (and _80 _83))
(define-fun _85 () Bool (and _75 _84))
(define-fun _86 () Bool (and _72 _85))
(define-fun _87 () Real |__ADDRESS_OF_main::var_group1|)
(define-fun _88 () Real (__BASE_ADDRESS_OF__ _87))
(define-fun _89 () Bool (= _87 _88))
(define-fun _90 () Bool (and _86 _89))
(define-fun _91 () Real |__ADDRESS_OF_main::var_memory_get_max_bandwidth_0_p1|)
(define-fun _92 () Real (__BASE_ADDRESS_OF__ _91))
(define-fun _93 () Bool (= _91 _92))
(define-fun _94 () Bool (and _90 _93))
(define-fun _95 () Real |__ADDRESS_OF_main::var_memory_get_cur_bandwidth_1_p1|)
(define-fun _96 () Real (__BASE_ADDRESS_OF__ _95))
(define-fun _97 () Bool (= _95 _96))
(define-fun _98 () Bool (and _94 _97))
(define-fun _99 () Real |__ADDRESS_OF_main::var_memory_set_cur_bandwidth_2_p1|)
(define-fun _100 () Real (__BASE_ADDRESS_OF__ _99))
(define-fun _101 () Bool (= _99 _100))
(define-fun _102 () Bool (and _98 _101))
(define-fun _103 () Real |__ADDRESS_OF_main::var_group2|)
(define-fun _104 () Real (__BASE_ADDRESS_OF__ _103))
(define-fun _105 () Bool (= _103 _104))
(define-fun _106 () Bool (and _102 _105))
(define-fun _107 () Real |__ADDRESS_OF_main::tmp|)
(define-fun _108 () Real (__BASE_ADDRESS_OF__ _107))
(define-fun _109 () Bool (= _107 _108))
(define-fun _110 () Bool (and _106 _109))
(define-fun _111 () Real |__ADDRESS_OF_main::tmp___0|)
(define-fun _112 () Real (__BASE_ADDRESS_OF__ _111))
(define-fun _113 () Bool (= _111 _112))
(define-fun _114 () Bool (and _110 _113))
(define-fun _115 () Real |__ADDRESS_OF_main::tmp___1|)
(define-fun _116 () Real (__BASE_ADDRESS_OF__ _115))
(define-fun _117 () Bool (= _115 _116))
(define-fun _118 () Bool (and _114 _117))
(define-fun _120 () Real |__ADDRESS_OF_intel_menlow_module_init::result|)
(define-fun _121 () Real (__BASE_ADDRESS_OF__ _120))
(define-fun _122 () Bool (= _120 _121))
(define-fun _123 () Bool (and _118 _122))
(define-fun _124 () Real |__ADDRESS_OF_intel_menlow_module_init::status|)
(define-fun _125 () Real (__BASE_ADDRESS_OF__ _124))
(define-fun _126 () Bool (= _124 _125))
(define-fun _127 () Bool (and _123 _126))
(define-fun _128 () Real |__ADDRESS_OF_intel_menlow_module_init::enable|)
(define-fun _129 () Real (__BASE_ADDRESS_OF__ _128))
(define-fun _130 () Bool (= _128 _129))
(define-fun _133 () Real (- 156))
(define-fun _134 () Bool (<= _73 _133))
(define-fun _135 () Bool (not _134))
(define-fun _136 () Real (* (- 1) _128))
(define-fun _137 () Real (+ _73 _136))
(define-fun _138 () Bool (<= _137 _133))
(define-fun _139 () Bool (and _135 _138))
(define-fun _140 () Bool (and _130 _139))
(define-fun _141 () Bool (and _127 _140))
(define-fun _142 () Real |__ADDRESS_OF_intel_menlow_module_init::__cil_tmp4|)
(define-fun _143 () Real (__BASE_ADDRESS_OF__ _142))
(define-fun _144 () Bool (= _142 _143))
(define-fun _145 () Bool (and _141 _144))
(define-fun _146 () Real |__ADDRESS_OF_intel_menlow_module_init::__cil_tmp5|)
(define-fun _147 () Real (__BASE_ADDRESS_OF__ _146))
(define-fun _148 () Bool (= _146 _147))
(define-fun _149 () Bool (and _145 _148))
(define-fun _150 () Real |__ADDRESS_OF_intel_menlow_module_init::__cil_tmp6|)
(define-fun _151 () Real (__BASE_ADDRESS_OF__ _150))
(define-fun _152 () Bool (= _150 _151))
(define-fun _153 () Bool (and _149 _152))
(define-fun _154 () Real |__ADDRESS_OF_intel_menlow_module_init::__cil_tmp7|)
(define-fun _155 () Real (__BASE_ADDRESS_OF__ _154))
(define-fun _156 () Bool (= _154 _155))
(define-fun _157 () Bool (and _153 _156))
(define-fun _158 () Real |__ADDRESS_OF_intel_menlow_module_init::__cil_tmp8|)
(define-fun _159 () Real (__BASE_ADDRESS_OF__ _158))
(define-fun _160 () Bool (= _158 _159))
(define-fun _161 () Bool (and _157 _160))
(define-fun _162 () Real |__ADDRESS_OF_intel_menlow_module_init::__cil_tmp9|)
(define-fun _163 () Real (__BASE_ADDRESS_OF__ _162))
(define-fun _164 () Bool (= _162 _163))
(define-fun _165 () Bool (and _161 _164))
(define-fun _166 () Real |__ADDRESS_OF_intel_menlow_module_init::__cil_tmp10|)
(define-fun _167 () Real (__BASE_ADDRESS_OF__ _166))
(define-fun _168 () Bool (= _166 _167))
(define-fun _169 () Bool (and _165 _168))
(define-fun _170 () Real |__ADDRESS_OF_intel_menlow_module_init::__cil_tmp11|)
(define-fun _171 () Real (__BASE_ADDRESS_OF__ _170))
(define-fun _172 () Bool (= _170 _171))
(define-fun _173 () Bool (and _169 _172))
(define-fun _174 () Real |__ADDRESS_OF_intel_menlow_module_init::__cil_tmp12|)
(define-fun _175 () Real (__BASE_ADDRESS_OF__ _174))
(define-fun _176 () Bool (= _174 _175))
(define-fun _177 () Bool (and _173 _176))
(define-fun _178 () Real (- 19))
(define-fun _179 () Real |intel_menlow_module_init::result@3|)
(define-fun _180 () Bool (= _179 _178))
(define-fun _181 () Bool (and _177 _180))
(define-fun _182 () Real acpi_disabled@2)
(define-fun _183 () Bool (= _182 _7))
(define-fun _187 () Bool (and _181 _183))
(define-fun _188 () Real |intel_menlow_module_init::__cil_tmp4@3|)
(define-fun _189 () Bool (= _188 _7))
(define-fun _190 () Bool (and _187 _189))
(define-fun _191 () Real (__string__ _7))
(define-fun _192 () Real |intel_menlow_module_init::__cil_tmp5@3|)
(define-fun _193 () Bool (= _191 _192))
(define-fun _194 () Bool (and _190 _193))
(define-fun _195 () Real |intel_menlow_module_init::__cil_tmp6@3|)
(define-fun _196 () Bool (= _195 _7))
(define-fun _197 () Bool (and _194 _196))
(define-fun _198 () Real (*unsigned_long_long_int@1 _128))
(define-fun _199 () Real |intel_menlow_module_init::enable@2|)
(define-fun _200 () Bool (= _198 _199))
(define-fun _201 () Real (acpi_evaluate_integer _188 _192 _195 _128))
(define-fun _202 () Real |intel_menlow_module_init::status@3|)
(define-fun _203 () Bool (= _201 _202))
(define-fun _204 () Bool (and _200 _203))
(define-fun _205 () Bool (and _197 _204))
(define-fun _206 () Bool (= _202 _7))
(define-fun _207 () Bool (not _206))
(define-fun _209 () Bool (and _205 _207))
(define-fun _210 () Bool (and _205 _206))
(define-fun _211 () Real |intel_menlow_module_init::__cil_tmp7@3|)
(define-fun _212 () Bool (= _128 _211))
(define-fun _213 () Bool (and _210 _212))
(define-fun _214 () Real (*unsigned_long_long_int@1 _211))
(define-fun _215 () Real |intel_menlow_module_init::__cil_tmp8@3|)
(define-fun _216 () Bool (= _214 _215))
(define-fun _217 () Bool (and _213 _216))
(define-fun _218 () Bool (= _215 _7))
(define-fun _220 () Bool (and _217 _218))
(define-fun _221 () Bool (not _218))
(define-fun _222 () Bool (and _217 _221))
(define-fun _223 () Real (acpi_bus_register_driver _45))
(define-fun _224 () Real |intel_menlow_module_init::result@4|)
(define-fun _225 () Bool (= _223 _224))
(define-fun _226 () Bool (and _222 _225))
(define-fun _227 () Bool (= _224 _7))
(define-fun _228 () Bool (not _227))
(define-fun _230 () Bool (and _226 _228))
(define-fun _231 () Bool (and _226 _227))
(define-fun _232 () Real 18446744073709551615)
(define-fun _233 () Real |intel_menlow_module_init::__cil_tmp9@3|)
(define-fun _234 () Bool (= _233 _232))
(define-fun _235 () Bool (and _231 _234))
(define-fun _236 () Real |intel_menlow_module_init::__cil_tmp10@3|)
(define-fun _237 () Bool (= _236 _7))
(define-fun _238 () Bool (and _235 _237))
(define-fun _239 () Real |intel_menlow_module_init::__cil_tmp11@3|)
(define-fun _240 () Bool (= _239 _7))
(define-fun _241 () Bool (and _238 _240))
(define-fun _242 () Real |intel_menlow_module_init::__cil_tmp12@3|)
(define-fun _243 () Bool (= _242 _7))
(define-fun _244 () Bool (and _241 _243))
(define-fun _245 () Real 13)
(define-fun _246 () Real 4294967295)
(define-fun _247 () Real __ADDRESS_OF_intel_menlow_register_sensor)
(define-fun _248 () Real (|*unsigned_int_((void)*,_unsigned_int,_(void)*,_((void)*)*)@1| _247))
(define-fun _249 () Real intel_menlow_register_sensor@1)
(define-fun _250 () Bool (= _248 _249))
(define-fun _253 () Real (- 8))
(define-fun _254 () Bool (<= _128 _253))
(define-fun _255 () Bool (not _254))
(define-fun _256 () Real (* (- 1) _247))
(define-fun _257 () Real (+ _128 _256))
(define-fun _258 () Bool (<= _257 _253))
(define-fun _259 () Bool (and _255 _258))
(define-fun _260 () Real (acpi_walk_namespace _245 _233 _246 _247 _236 _239 _242))
(define-fun _261 () Real |intel_menlow_module_init::status@4|)
(define-fun _262 () Bool (= _260 _261))
(define-fun _263 () Bool (and _250 _259))
(define-fun _264 () Bool (and _262 _263))
(define-fun _265 () Bool (and _244 _264))
(define-fun _266 () Bool (= _261 _7))
(define-fun _267 () Bool (not _266))
(define-fun _269 () Bool (and _265 _267))
(define-fun _270 () Bool (and _265 _266))
(define-fun _271 () Real |intel_menlow_module_init::__retval__@2|)
(define-fun _272 () Bool (= _271 _7))
(define-fun _273 () Bool (and _270 _272))
(define-fun _275 () Bool (= _271 _178))
(define-fun _276 () Bool (and _269 _275))
(define-fun _277 () Bool (or _273 _276))
(define-fun _278 () Bool (= _224 _271))
(define-fun _279 () Bool (and _230 _278))
(define-fun _280 () Real |intel_menlow_module_init::__cil_tmp10@2|)
(define-fun _281 () Bool (= _236 _280))
(define-fun _282 () Real |intel_menlow_module_init::__cil_tmp11@2|)
(define-fun _283 () Bool (= _239 _282))
(define-fun _284 () Bool (and _281 _283))
(define-fun _285 () Real |intel_menlow_module_init::__cil_tmp12@2|)
(define-fun _286 () Bool (= _242 _285))
(define-fun _287 () Bool (and _284 _286))
(define-fun _288 () Real |intel_menlow_module_init::__cil_tmp9@2|)
(define-fun _289 () Bool (= _233 _288))
(define-fun _290 () Bool (and _287 _289))
(define-fun _291 () Bool (= _202 _261))
(define-fun _292 () Bool (and _290 _291))
(define-fun _293 () Real |__ADDRESS_OF___VERIFIER_fake_alloc*(void)[0]#0|)
(define-fun _294 () Real (* (- 1) _293))
(define-fun _295 () Real (+ _128 _294))
(define-fun _296 () Bool (<= _295 _253))
(define-fun _297 () Bool (and _255 _296))
(define-fun _299 () Bool (<= _247 _253))
(define-fun _300 () Bool (not _299))
(define-fun _301 () Real (+ _247 _294))
(define-fun _302 () Bool (<= _301 _253))
(define-fun _303 () Bool (and _300 _302))
(define-fun _304 () Bool (and _297 _303))
(define-fun _305 () Bool (and _279 _292))
(define-fun _306 () Bool (or _277 _305))
(define-fun _307 () Bool (and _304 _306))
(define-fun _308 () Bool (and _220 _275))
(define-fun _309 () Bool (= _179 _224))
(define-fun _310 () Bool (and _290 _309))
(define-fun _311 () Bool (and _291 _310))
(define-fun _312 () Real |__ADDRESS_OF___VERIFIER_fake_alloc*(void)[0]#1|)
(define-fun _313 () Real (* (- 1) _312))
(define-fun _314 () Real (+ _128 _313))
(define-fun _315 () Bool (<= _314 _253))
(define-fun _316 () Bool (and _255 _315))
(define-fun _317 () Bool (<= _293 _7))
(define-fun _318 () Bool (not _317))
(define-fun _319 () Bool (<= _293 _312))
(define-fun _320 () Bool (and _318 _319))
(define-fun _321 () Bool (and _316 _320))
(define-fun _322 () Bool (and _308 _311))
(define-fun _323 () Bool (or _307 _322))
(define-fun _324 () Bool (and _321 _323))
(define-fun _325 () Bool (and _209 _275))
(define-fun _326 () Real |intel_menlow_module_init::__cil_tmp7@2|)
(define-fun _327 () Bool (= _211 _326))
(define-fun _328 () Bool (and _287 _327))
(define-fun _329 () Real |intel_menlow_module_init::__cil_tmp8@2|)
(define-fun _330 () Bool (= _215 _329))
(define-fun _331 () Bool (and _328 _330))
(define-fun _332 () Bool (and _289 _331))
(define-fun _333 () Bool (and _309 _332))
(define-fun _334 () Bool (and _291 _333))
(define-fun _335 () Real |__ADDRESS_OF___VERIFIER_fake_alloc*(void)[0]#2|)
(define-fun _336 () Real (* (- 1) _335))
(define-fun _337 () Real (+ _128 _336))
(define-fun _338 () Bool (<= _337 _253))
(define-fun _339 () Bool (and _255 _338))
(define-fun _340 () Bool (<= _312 _7))
(define-fun _341 () Bool (not _340))
(define-fun _342 () Bool (<= _312 _335))
(define-fun _343 () Bool (and _341 _342))
(define-fun _344 () Bool (and _339 _343))
(define-fun _345 () Bool (and _325 _334))
(define-fun _346 () Bool (or _324 _345))
(define-fun _347 () Bool (and _344 _346))
(define-fun _348 () Real |main::tmp@3|)
(define-fun _349 () Bool (= _271 _348))
(define-fun _350 () Bool (and _347 _349))
(define-fun _351 () Bool (= _348 _7))
(define-fun _355 () Bool (and _350 _351))
(define-fun _356 () Real ___pc@4)
(define-fun _357 () Bool (= _356 _14))
(define-fun _358 () Bool (and _355 _357))


(push 1)
(assert _2)
(set-info :status unsat)
(check-sat)
(pop 1)
(push 1)
(assert _358)
(set-info :status sat)
(check-sat)
(pop 1)
(exit)
